ePMC

Benchmark
Model:wlan v.1 (MDP)
Parameter(s)MAX_BACKOFF = 5, COL = 0
Property:sent (prob-reach)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files wlan.5.prism --model-input-type prism --property-input-files wlan.props --property-input-names sent --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const COL=0
Execution
Walltime:92.54339742660522s
Return code:0
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property sent
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 17539 17538
build-model-states-explored 38325 20786
build-model-states-explored 57704 19379
build-model-states-explored 78571 20867
build-model-states-explored 103814 25243
build-model-states-explored 128164 24350
build-model-states-explored 152140 23976
build-model-states-explored 177873 25733
build-model-states-explored 203443 25570
build-model-states-explored 227300 23857
build-model-states-explored 254535 27235
build-model-states-explored 281613 27078
build-model-states-explored 308516 26903
build-model-states-explored 335367 26851
build-model-states-explored 362896 27529
build-model-states-explored 390425 27529
build-model-states-explored 414904 24479
build-model-states-explored 438158 23254
build-model-states-explored 457686 19528
build-model-states-explored 480678 22991
build-model-states-explored 506109 25432
build-model-states-explored 531104 24995
build-model-states-explored 556032 24928
build-model-states-explored 581429 25397
build-model-states-explored 606657 25228
build-model-states-explored 632008 25351
build-model-states-explored 657140 25132
build-model-states-explored 679934 22794
build-model-states-explored 704347 24413
build-model-states-explored 731248 26901
build-model-states-explored 758123 26875
build-model-states-explored 784174 26051
build-model-states-explored 810307 26133
build-model-states-explored 832180 21873
build-model-states-explored 858595 26415
build-model-states-explored 885016 26421
build-model-states-explored 911440 26424
build-model-states-explored 937854 26414
build-model-states-explored 963662 25808
build-model-states-explored 990012 26350
build-model-states-explored 1015970 25958
build-model-states-explored 1042776 26806
build-model-states-explored 1069731 26955
build-model-states-explored 1097149 27417
build-model-states-explored 1124707 27559
build-model-states-explored 1152251 27544
build-model-states-explored 1179733 27482
build-model-states-explored 1207261 27527
build-model-states-explored 1234783 27523
build-model-states-explored 1262284 27501
build-model-states-explored 1287993 25709
build-model-done 1295218 51
iterating
iterating-progress-unbounded 74 2.0 1
iterating-progress-unbounded 155 2.0 2
iterating-progress-unbounded 236 2.0 3
iterating-progress-unbounded 317 2.0 4
iterating-progress-unbounded 397 1.0 5
iterating-progress-unbounded 477 1.0 6
iterating-progress-unbounded 556 1.0 7
iterating-progress-unbounded 635 1.0 8
iterating-progress-unbounded 714 1.0 9
iterating-progress-unbounded 792 1.0 10
iterating-progress-unbounded 869 1.0 11
iterating-progress-unbounded 947 1.0 12
iterating-progress-unbounded 1024 1.0 13
iterating-progress-unbounded 1102 0.3333333333333333 14
iterating-progress-unbounded 1179 0.02439161225371132 15
iterating-progress-unbounded 1257 0.01250174356474144 16
iterating-progress-unbounded 1334 0.008405215446395775 17
iterating-progress-unbounded 1411 0.006351282121171994 18
iterating-progress-unbounded 1489 0.00509105142599493 19
iterating-progress-unbounded 1566 0.004266341831113355 20
iterating-progress-unbounded 1643 0.003192438831761325 21
iterating-progress-unbounded 1721 0.0021708994332888952 22
iterating-progress-unbounded 1798 0.0015240883890394932 23
iterating-progress-unbounded 1876 0.0010440588228408196 24
iterating-progress-unbounded 1953 6.642055997669963E-4 25
iterating-progress-unbounded 2030 3.424798064012255E-4 26
iterating-progress-unbounded 2108 3.843586682636507E-5 27
iterating-progress-unbounded 2185 5.696406913818922E-6 28
iterating-progress-unbounded 2262 5.571712143269778E-6 29
iterating-progress-unbounded 2340 5.31249055849038E-6 30
iterating-progress-unbounded 2417 4.929105112679688E-6 31
iterating-progress-unbounded 2494 4.411442828427343E-6 32
iterating-progress-unbounded 2572 3.7578032002017044E-6 33
iterating-progress-unbounded 2649 2.985222686615321E-6 34
iterating-progress-unbounded 2726 2.1739834008913393E-6 35
iterating-progress-unbounded 2804 1.4844397201488589E-6 36
iterating-progress-unbounded 2881 9.348434106684553E-7 37
iterating-progress-unbounded 2958 5.11833282742824E-7 38
iterating-done 2962 38
model-checking-done 91
command-check-result-is true sent